a, b, c, d:. 0  a  0  c  a  b  c  d  a * c  b * d 

latex

Definitions	(i = j), qeq(r;s), ff, i <z j, tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.2, t.1, , x f y, if b then t else f fi , b, a  b, r * s, r  s, {T}, A c B, P  Q, P & Q, True, T, , P  Q, P  Q, t  T, P  Q, x:A. B(x), False, A, Dec(P), S  T
Lemmas	int-rational, qmul comm qrng, qmul preserves qle, qle weakening eq qorder, qle antisymmetry, qle-iff, and functionality wrt iff, decidable qless, decidable cand, qless wf, qle transitivity qorder, qmul-non-neg, qmul wf, qmul zero qrng, true wf, squash wf, rationals wf, int inc rationals, qle wf, decidable equal rationals